COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00014 00003	.skip 1
C00015 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.CB STATING THE CORRECTNESS OF LISP PROGRAMS


	In previous work on proving the correctness of LISP programs,
the properties proved have  been chosen somewhat opportunistically.
Thus we proved that %2append%1 is associative and that
%2reverse[u*v]_=_reverse_v_*_reverse_u%1 without claiming that these
properties in themselves constitute the "correctness" of ⊗append 
or ⊗reverse. 

	I don't believe there is any general way of expressing
what is intuitively meant by the "correctness" of a computer program.
However, particular classes of programming problems admit
ways of formalizing correctness in logic.

	Let us being with sort programs, because they have been
treated extensively in the program verification literature.
We shall begin with %2extensional correctness%1, i.e. a program
is extensionally correct if it gets the right answer, saying nothing
about how much space or time it uses.  Later we will discuss the
method of derived functions for getting what we are tempted to
call %2intensional correctness%1 but which probably more properly
called %2operational correctness%1 or %2computational correctness%1.

	In LISP we shall be dealing with functions defined by
conditional expression recursion, and the correctness is a relation
between the arguments and the value of the function.  Suppose %2sort_u%1
is a sort function.  Intuitively ⊗sort is extensionally correct if
for all lists ⊗u whose elements are from the appropriate domain,
%2sort_u%1 is defined and in ascending order and has the same
elements as ⊗u with the same multiplicities.  The problem is to
express this specification formally in such a way that a reader is
confident that these are the correct specifications without further
proof.  As stated above, there is always some uncertainty that
a formal specification means the same thing as an informal
natural language specification just as there is always residual
uncertainty that a natural language specification correctly expresss
what its writer "really meant".

	To begin with we want to say that ⊗sort_u is ordered.  One way
involves a LISP function ordered that may be written

!!a1:	%2ordered u ← qn u ∨ qn qd u ∨ [qa u ≤ qad u ∧ ordered qd u]%1.

We can then prescribe

!!a2:	%2ordered_sort_u%1.

If the recursive definition of ⊗sort is complicated, and the user is
facile enough with LISP to read ({eq a1}) easily, a proof of ({eq a2})
will substantially increase his confidence that ⊗sort meets this part of
its specification.  In fact, he may be ready to pay off on his contract
for the production of the sort program provided he is equally well
pleased with the other specifications.  Maybe his confidence can
be increased by a proof that ⊗ordered is total which can easily
be supplied.  It is not immediately clear what else could be
proved about the LISP predicate ⊗ordered by itself that would
increase his confidence, but if other functions and predicates
are available, proof of some relations among ⊗ordered and the
others may help.

	The relation ⊗istail between two lists will probably play
a fundamental role in the theory of LISP programs.  %2istail_u_v%1
is true if the list ⊗u can be obtained by deleting zero or more
elements from the front of ⊗v and has the LISP definition

!!a3:	%2u istail v ← qn u ∨ u = v ∨ u istail qd v%1.

	Its fundamental character is suggested by the fact that
if ⊗istail is added to the basic functions of LISP all other
LISP functions can be given explicit non-recursive definitions.
These definitions (described in McCarthy 1978)
are not computationally usable, because they involve quantifiers,
but may be important in proving correctness.  Anyway we can also
defined ⊗ordered by

!!a4:	%2ordered u ≡ ∀v1 v2.(v1 istail v2 ∧ v2 istail u ⊃ qa v1 ≤ qa v2)%1.

Although it is not recursive, it is not immediately clear to me that this
definition of ordered is more perspicuous than ({eq a1}), but there may be
some logical sense in which it is.  For example, certain proofs using
({eq a4}) may not require any kind of mathematical induction.

	The second part of the specification of a sort program is more
difficult.  We need to say that the sorted list and the original list have
the same elements with the same multiplicities.  One way is to say that
the two lists give rise to the same bag or multiset.  An obvious way to
represent the bag of a list is by sorting it, so if we have some abstract
way of defining sort, then we can state the correctness of ⊗sort by
demanding that it be equivalent.
	
	A more direct specification is

!!a5:	%2∀x.(multiplicity(x,u) = multiplicity(x,sort u))%1,

where ⊗multiplicity gets the LISP definition

!!a6:	%2multiplicity[x,u] ← qif qn u qthen 0 qelse qif x = qa u qthen
1 + multiplicity[x,qd u] qelse multiplicity[x,qd u]%1.

Another definition is

!!a7:	%2multiplicity(x,u) = card α{v | v istail u ∧ x = qa vα}%1.

This requires more set theory to manipulate it, but it might be thought
closer to the intuitive meaning of multiplicity.

	Another approach is to axiomatize bags and the function %2bag u%1
that gives the bag corresponding to a list.  We do not assume any
representation of bags, i.e. our bag language contains no notation for
arbitrary bag constants.  The axiomatization also involves a function
⊗mult(x,z) giving the multiplicity of the element ⊗x in the bag ⊗z.  Here
are some axioms and a schema:

	%2∀z1 z2.(∀x.(mult(x,z1) = mult(x,z2)) ⊃ z1 = z2)%1

	%2∀z x.(mult(x,adjoin(x,z)) = 1 + mult(x,z))%1

	%2∀x.(mult(x,Zerobag) = 0)%1

	%2qF(Zerobag) ∧ ∀x z.(qF(z) ⊃ qF(adjoin(x,z))) ⊃ ∀z.qF(z)%1

	%2∀u.(bag u = qif qn u qthen Zerobag qelse adjoin(qa u, bag qd u))%1

At some point we are dependent on a theorem or metatheorem to the effect
that the axiomatized functions exist.  This can be demonstrated by
representing them as sorted lists and proving that some sort function
satisfies the axioms for %2bag_u%1.

	(If I understand it correctly, the Stanford Verification Group's
treatment of sorting involves axiomatizing the predicate %2permutes(u,v)%1
which asserts that the array ⊗A is a permutation of the array ⊗B.  This
seems to me to be more peculiar to sorting and hence more ad hoc than the
approaches suggested here).

	Some programs can be proved correct by showing that there
is a unique program that has some of the specifications that it is
agreed that the program should have.  Thus ⊗u*v can be characterized
by the properties %2qnil * v = v%1 and %2[x . u] * v = x . [u * v]%1.
The uniqueness of ⊗u*v satisfying these conditions is established
by proving that

!!a:	%2u * v ← qif qn u qthen v qelse qa u . [qd u * v]%1

is total.

	An alternate characterization is that %2qnil * v = v, <x>*v = x.v%1,
and associativity %2u*[v*w] = [u*v]*w%1.  We can again prove that ⊗u*v 
is the unique function that satisfies these conditions.  The easiest way
is to prove that anything that satisfies the second set of conditions
also satisfies the first set of conditions.  This follows since we can
write %2[x.u]*v = [<x>*u]*v = <x>[u*v] = x.[u*v].  We must then prove that
({eq a}) is total and satisfies the second set of conditions.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
CORREC[S78,JMC]
PUBbed at {time} on {date}.%1